…sults to the environment (#92)

### Description:

Forewarning: the diff of this one is rather large.

I've implemented a new version of step theorem generation, culminating
in the `genStepEqTheorem` function.

In particular:
- We get rid of the different fetch/decode/exec intermediate lemma,
instead opting to generate the final step theorem in one go. The
bottleneck seems to be kernel checking, so by reducing the number of
theorems sent to the kernel we achieve a good speedup (SHA512 used to
take about 55 seconds for the three generation commands combined, now
it's about 35 seconds).
- In the process, we build a `ProgramInfo` struct, which holds a bunch
of interesting expressions that further proof automation could exploit.
This programInfo is stored in a persistent environment extension, so
that it is persisted in the olean files (hence, making it available to
downstream files).
- While building the previous, I've moved some definitions around and
did other refactors: happy to split those off into their own PR if that
makes reviewing easier.

EDIT: split off #93 for the `#time` command

### Testing:

`make all` succeeded

### License:

By submitting this pull request, I confirm that my contribution is
made under the terms of the Apache 2.0 license.

---------

Co-authored-by: Siddharth <[email protected]>
Co-authored-by: Shilpi Goel <[email protected]>